\chapter{Conclusions and future work}
\label{future}
The contextual transformation is one of the most complex transformation step of the \K definition compiler. In this dissertation we analyzed it and we got the following results:
\begin{itemize}
\item A formal definition of witness sets.
\item An algorithm for finding the witness sets.
\item Two algorithms for finding all possible contexts for a given rule using witness sets.
\item A formal definition of locality principle.
\item Consistency checks and filters for disambiguation.
\item An algorithm for finding the final unambiguous context of a rule. 
\end{itemize}
These are basic elements for getting the context of a \K rule. There are also other problems which have to be solved when doing context transformers. Cell creation/deletion are special cases of transformations: when splitting rule in rhs and lhs we have to keep additional information about the {\it rewrite points} (nodes which are created/deleted). Consider the following rule:
\begin{verbatim}
               rule . => <cell> .Bag </cell>
\end{verbatim}
How can we apply context transformers on this rule? We can observe that splitting the rule into lhs and rhs causes more problems because the lhs is "\verb=.=" and we do not have any information about it. Supposing we have somehow the contexts for both lhs and rhs how can we combine them? What are the nodes which have to be rewritten? The answer of these questions stays in storing more information about cell involved in rewrite operations before splitting the rule. Also, looking on the other side could help when finding the context of "\verb=.=". In our case, the context of "\verb=.=" is given by the first (bottom-up) parent of cell {\it cell} which has multiplicity {\it ANY} or {\it SOME}. \\

Another issue is related to lhs and rhs. Because they are separate trees we can find contexts for each of them but we have to merge them back. The other transformations depend on this merging. The problem is that if at least one of them is ambiguous then we have to disambiguate. When merging, we should also take care of compatibility of contexts for lhs and rhs which is not necessarily easy.
In conclusion, the actual work on contextual transformation has been qualitatively improved by the results obtained in this dissertation. After including the special cases discussed above in the algorithm implemented by Function \ref{a4}, it is ready to be used in the new version of \K Framework.